T:Type, L1, L2, L:T List, f1:(||L1||||L||), f2:(||L2||||L||).
interleaving_occurence(T;L1;L2;L;f1;f2)  Prop 

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, ij, P  Q, False, A, AB, , Prop, l[i], S  T, S  T, increasing(f;k), P & Q, interleaving_occurence(T;L1;L2;L;f1;f2)
Lemmas	nat wf, increasing wf, select wf, not wf, non neg length, int seg wf, length wf1